half(0) → 0
half(s(s(x))) → s(half(x))
log(s(0)) → 0
log(s(s(x))) → s(log(s(half(x))))
↳ QTRS
↳ DependencyPairsProof
half(0) → 0
half(s(s(x))) → s(half(x))
log(s(0)) → 0
log(s(s(x))) → s(log(s(half(x))))
LOG(s(s(x))) → HALF(x)
HALF(s(s(x))) → HALF(x)
LOG(s(s(x))) → LOG(s(half(x)))
half(0) → 0
half(s(s(x))) → s(half(x))
log(s(0)) → 0
log(s(s(x))) → s(log(s(half(x))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
LOG(s(s(x))) → HALF(x)
HALF(s(s(x))) → HALF(x)
LOG(s(s(x))) → LOG(s(half(x)))
half(0) → 0
half(s(s(x))) → s(half(x))
log(s(0)) → 0
log(s(s(x))) → s(log(s(half(x))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
HALF(s(s(x))) → HALF(x)
half(0) → 0
half(s(s(x))) → s(half(x))
log(s(0)) → 0
log(s(s(x))) → s(log(s(half(x))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
HALF(s(s(x))) → HALF(x)
The value of delta used in the strict ordering is 35/8.
POL(HALF(x1)) = x_1
POL(s(x1)) = 5/4 + (5/2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
half(0) → 0
half(s(s(x))) → s(half(x))
log(s(0)) → 0
log(s(s(x))) → s(log(s(half(x))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
LOG(s(s(x))) → LOG(s(half(x)))
half(0) → 0
half(s(s(x))) → s(half(x))
log(s(0)) → 0
log(s(s(x))) → s(log(s(half(x))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LOG(s(s(x))) → LOG(s(half(x)))
The value of delta used in the strict ordering is 15.
POL(half(x1)) = 1 + (5/4)x_1
POL(LOG(x1)) = (4)x_1
POL(s(x1)) = 4 + (5/4)x_1
POL(0) = 7/4
half(0) → 0
half(s(s(x))) → s(half(x))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
half(0) → 0
half(s(s(x))) → s(half(x))
log(s(0)) → 0
log(s(s(x))) → s(log(s(half(x))))